g:IMonoid, n:|(<+>hgrp)|, e:|g|. (n  e)  |g| 

latex

Up	groups 1
Definitions of Statement	|g|, , e, IMonoid, Mon, AbMon, Group{i}, AbGrp, OCMon, a  b, OGrp, |g|, ghgrp, <+>
Definitions	t  T, x:A. B(x), , IMonoid, Mon, Group{i}, AbGrp, t.1, |g|, ghgrp, |g|, , P & Q, P  Q, P  Q, t.2, , x f y, e, a  b, <+>
Lemmas	imon wf, int add grp wf2, hgrp of ocgrp wf, grp car wf, abgrp wf, int add grp wf, hgrp car properties, le wf, mon nat op wf, assert of le int